T:Type, x:T, L, L1, L2:T List.
interleaving(T;L1;L2;x.L)

0<||L1|| & L1[0] = x & interleaving(T;tl(L1);L2;L)
 0<||L2|| & L2[0] = x & interleaving(T;L1;tl(L2);L) 

latex

Definitions

increasing(f;k), S  T, S  T, b, , Unit, Inj(A; B; f), if b t else f fi, i  j < k, {i..j}, T, x:A. B(x), disjoint_sublists(T;L1;L2;L), True, ij, hd(l), i<j, ij, {T}, SQType(T), , P  Q, tl(l), ||as||, P  Q, False, A, AB, interleaving(T;L1;L2;L), l[i], P & Q, Prop, A & B, P  Q, t  T, x:A. B(x), P  Q, Dec(P), null(as), b

Lemmas

decidable assert, null wf, assert of null, iff wf, length wf1, select wf, interleaving wf, tl wf, length wf2, le wf, cons one one, non neg length, nil interleaving, nat wf, member wf, nil interleaving2, true wf, not wf, false wf, non nil length, not functionality wrt iff, assert wf, decidable int equal, int seg wf, injection le, length cons, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, bnot of lt int, assert of le int, lt int wf, bool wf, le int wf, bnot wf, increasing implies, increasing inj, increasing implies le, decidable lt, length zero, length tl, increasing wf, select cons tl, select tl, cons interleaving, cons interleaving2